(set-logic QF_UFLRA)
(set-info :source |CPAchecker with k-induction on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)


(declare-fun |main::y@2| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun |__ADDRESS_OF_main::x| () Real)
(declare-fun |main::n@3| () Real)
(declare-fun |__ADDRESS_OF_main::y| () Real)
(declare-fun |__ADDRESS_OF_main::n| () Real)
(declare-fun |main::x@2| () Real)
(declare-fun |__VERIFIER_assert::cond@2| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real |__ADDRESS_OF_main::n|)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real |__ADDRESS_OF_main::x|)
(define-fun _12 () Real (__BASE_ADDRESS_OF__ _11))
(define-fun _13 () Bool (= _11 _12))
(define-fun _14 () Real |main::n@3|)
(define-fun _15 () Real |main::x@2|)
(define-fun _16 () Bool (= _14 _15))
(define-fun _17 () Bool (and _13 _16))
(define-fun _18 () Bool (and _10 _17))
(define-fun _19 () Real |__ADDRESS_OF_main::y|)
(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19))
(define-fun _21 () Bool (= _19 _20))
(define-fun _22 () Real |main::y@2|)
(define-fun _23 () Bool (= _22 _7))
(define-fun _24 () Bool (and _21 _23))
(define-fun _25 () Bool (and _18 _24))
(define-fun _26 () Bool (<= _15 _7))
(define-fun _28 () Real 1)
(define-fun _31 () Bool (and _25 _26))
(define-fun _32 () Bool (= _14 _22))
(define-fun _33 () Real (ite _32 _28 _7))
(define-fun _34 () Real |__VERIFIER_assert::cond@2|)
(define-fun _35 () Bool (= _33 _34))
(define-fun _36 () Bool (and _31 _35))
(define-fun _37 () Bool (= _34 _7))
(define-fun _39 () Bool (and _36 _37))



(assert _39)
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
